package typechecker;

import java.util.Arrays;
import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import java.util.Queue;
import java.util.Set;
import java.util.Vector;

public class ConstraintGraph {	
	/* Variable name to variable index mappings */
	private Map<String,Integer> varSet = new HashMap<String,Integer>();
	private Vector<String> vars = new Vector<String>();

	/* Graph structure  */
	private Vector<LinkedList<Integer>> dnNeigh = new Vector<LinkedList<Integer>>();
	private Vector<LinkedList<Integer>> upNeigh = new Vector<LinkedList<Integer>>();
	private List<Edge> edges = new LinkedList<Edge>();

	private final int INFINITY_INDEX = getVarIndex(Stage.INFINITY);
	
	/**
	 * The function wich checks termination of recursive definitions.
	 * 
	 * @param a	The stage variable which coresponds to the recursive argument
	 * and which must be mapped to a fresh stage variable 
	 * @param vStarNo The set of stage variables which must be mapped to a stage
	 * expression with the same base variable as {@link a} 
	 * @param v The set v \ vStar must be mapped to stage expressions with
	 * different stage variables than {@link a}
	 * 
	 */
	public void recCheck(Stage a, Set<Integer> vStarNo, Set<Integer> v){
		Set<Integer> vDiff = new HashSet<Integer>();
		Set<Integer> vStar = new HashSet<Integer>();
		for( int  i : vStarNo){
			vStar.add(getVarIndex(new Stage("v"+i,0)));
		}
//		printCol("vSTar", vStar);
		for( int i : v){
			vDiff.add(getVarIndex(new Stage("v"+i,0)));
		}
		vDiff.removeAll(vStar);
		int alpha = getVarIndex(a);
		recCheckImpl(alpha, vStar, vDiff);
	}	
	
	private void recCheckImpl(int a, Set<Integer> vStar , Set<Integer> vDiff){
		/* 1. Si := downwards closure of V* */
		Set<Integer> si = this.upDownClosure(this.dnNeigh, vStar);

		/* 2. add constaints : a < x , \/ x in Si. */
		for (int  x:  si)
			this.addZeroConstaint(a, x);
		
		/* 3. removes one negative cycle a time, until there are no more of them */
		while( this.negativeCycleRemoval());


		// 4. Si< := upwards closure of Si (var to be mapped to [i] or Inf. 
		Set<Integer> siGT = this.upDownClosure(this.upNeigh, si);
		
		// 5. S!i := upwards closure of VDiff */
		Set<Integer> siDIFF = this.upDownClosure(this.upNeigh, vDiff);
		
		// 6. map S!i /\ Si< --> Inf => constaints 
		siGT.retainAll(siDIFF);
		for( int x  : siGT)
			this.addZeroConstaint(INFINITY_INDEX , x);
		
		/* 7. SInf := upwards closure of Inf */
		Set<Integer> sInf = this.upDownClosure(upNeigh, new HashSet<Integer>(Arrays.asList(INFINITY_INDEX)));
		
		/* 8. asserts that SInf /\ Si != 0, and returns the constraints */
		sInf.retainAll(si);
		if( !sInf.isEmpty()){
			throw new TypeCheckingException("Universally quantified variable "+ vars.get(a) + " mapped to infty by the constraint solution");
		}
	}

	/**
	 * Computes the upwards or downwards closure of a set of nodes in the 
	 * graph
	 * @param neighbors The neighbours of each node in the desired direction
	 *  (up/down)
	 * @param m The set whose closure is to be calculated
	 * @return 
	 */
	private Set<Integer> upDownClosure(Vector<LinkedList<Integer>> neighbors , Set<Integer> m){
		Queue<Integer> bfsList = new LinkedList<Integer>();
		Set<Integer> ret = new HashSet<Integer>();
		
		for( int root : m){
			bfsList.clear();
			bfsList.add(root);
			
			while( ! bfsList.isEmpty()){
				Integer crt = bfsList.poll();
				boolean is_new = ret.add(crt);
				
				if( is_new){
					bfsList.addAll(neighbors.get(crt));
				}
			}
		}
		return ret;
	}
	
	
	private boolean negativeCycleRemoval(){
		int n = vars.size(), root = n;
		int dist [] = new int [n + 1];
		int pred [] = new int [n + 1];
		Arrays.fill(dist, Integer.MAX_VALUE/2);
		dist[root] = 0;

		/* we add a new root connected to each other vertex */
		Vector<Edge> es = new Vector<Edge>(edges);
		for( int v = 0 ; v < n; v++){
			es.add(new Edge(root,v, 1));
		}
		
		/* relax the edges N-1 times*/
		for( int v = 0 ; v < n-1; v++){
			for(Edge e : es){
				if(dist[e.s1] + e.diff < dist[e.s2]){
					dist[e.s2] = dist[e.s1] + e.diff; 
					pred[e.s2] = e.s1;
				}
			}
		}
		
		/* 
		 * If there is a  edge that can be relaxed further, then there is a
		 * negative cycle. 
		 */
		int beta = -1;
		for(Edge e : es){
			if(dist[e.s1] + e.diff < dist[e.s2]){
//				System.out.println("Found a negative cycle!");
				Set<Integer> cycle = new HashSet<Integer>();
				beta = e.s2;
				while(cycle.add(beta)){
					beta = pred[beta];
				}

//				for(int i : cycle)
//					System.out.print(vars.get(i)+" -> ");
//				System.out.println();
				break;
			}
		}

		if( beta != -1){
			Set<Integer> betaGT = upDownClosure(this.upNeigh, new HashSet<Integer>(Arrays.asList(beta)));
			/* removes any edge between to nodes on the cycle */
			for( Iterator<Edge> i = edges.iterator(); i.hasNext(); ){
				Edge e = i.next();
				if( betaGT.contains(e.s1) ||  betaGT.contains(e.s2) ){
					i.remove();
					dnNeigh.get(e.s1).removeFirstOccurrence(e.s2);
					upNeigh.get(e.s2).removeFirstOccurrence(e.s1);
				}
			}
			/* map any element greater than that cycle to infinity */
			for( int x : betaGT){
				this.addZeroConstaint(INFINITY_INDEX , x);
			}
			return true;
		}
		return false;
	}
	
	public void simplify(){
		Set<Integer> sInf =  this.upDownClosure(upNeigh, new HashSet<Integer>(Arrays.asList(INFINITY_INDEX)));
		removeInfEdges(sInf);
		for( int i : sInf){
			this.addZeroConstaint(INFINITY_INDEX, i);
		}
	}
	
	private void removeInfEdges(Set<Integer> sInf){
		for( Iterator<Edge> i = edges.iterator(); i.hasNext(); ){
			Edge e = i.next();
			if( e.s1 == INFINITY_INDEX || sInf.contains(e.s1) || sInf.contains(e.s2)){
				i.remove();
				dnNeigh.get(e.s1).removeFirstOccurrence(e.s2);
				upNeigh.get(e.s2).removeFirstOccurrence(e.s1);
			}
		}	
	}
	/**
	 * Adds the constraint a < b to the constraint graph.
	 */
	public void addConstraint(Stage a , Stage b){
		/* constraints in NT are not added */
		if( !checkNT(a , b)){
			return;
		}
		/* trivially satisfied */
		if( b.isInfinity()){
			return; 
		}
		int idxa = getVarIndex(a);
		int idxb = getVarIndex(b);
		int diffba = 0;
		
		if(idxa == idxb && a.getSucc() <= b.getSucc())
			return;
		if( a.isInfinity()){
			diffba = 0;
		}
		else{
			diffba = b.getSucc() - a.getSucc();
		}
		Edge e = new Edge(idxb, idxa, diffba);
		if(edges.contains(e))
			return;
		
		edges.add(e);
		dnNeigh.get(idxb).add(idxa);
		upNeigh.get(idxa).add(idxb);
		//System.out.print("added edge in " + this.hashCode() +" : " + preetyPrintEdge(e) );
	}
	
	/* This functions assumes that indexes are valid */
	private void addZeroConstaint(int idxa, int idxb ){
		Edge e = new Edge(idxb, idxa, 0);
		if(edges.contains(e))
			return;
		if(idxa == idxb )
			return;
		edges.add(e);
		dnNeigh.get(idxb).add(idxa);
		upNeigh.get(idxa).add(idxb);
	}
	
	private boolean checkNT(Stage a , Stage b){
		if((b == Stage.NONTERM && a != Stage.NONTERM) || (a == Stage.NONTERM && b != Stage.NONTERM)){
			throw new TypeCheckingException("Trying to compare NT and ID types",true);
		}
		if( a != Stage.NONTERM && b != Stage.NONTERM){
			return true;
		}
		return false;
	}
	/**
	 * Finds the index of a given stage variable in the
	 * internal vector, and adds it if not already there.
	 */
	private int getVarIndex(String s){
		Integer idx = varSet.get(s);
		if(idx == null){
			idx = vars.size();
			vars.add(s);
			dnNeigh.add(new LinkedList<Integer>());
			upNeigh.add(new LinkedList<Integer>());
			varSet.put(s, idx);
		}
		return idx;
		
	}
	
	private int getVarIndex(Stage s){
		return getVarIndex(s.getBaseVar());
	}	
		
	@Override
	public String toString() {
		return this.preetyPrint();
	}
	
	public String preetyPrint(){
		StringBuffer sbf = new StringBuffer();
		sbf.append(edges.size() + " constaints:\n");
		for( Edge e : edges){
			sbf.append(preetyPrintEdge(e));
		}
		return sbf.toString();
	}
	
	private String preetyPrintEdge(Edge e){
		StringBuffer sbf = new StringBuffer();
		
		sbf.append("{");
		for(int i = e.diff; i < 0; i++)
			sbf.append("s ");
		sbf.append(vars.get(e.s2));
		sbf.append("\t<\t");
		for(int i = 0; i < e.diff; i++)
			sbf.append("s ");
		sbf.append(vars.get(e.s1));
		sbf.append("}\n");	
		
		return sbf.toString();
	}	

	void printCol(String s, Collection<Integer> c){
		System.out.print(s + " : ");
		for(int i: c){
			System.out.print(vars.get(i)+ " ");
		}
		System.out.println();
	}
	
	public ConstraintGraph addAll(ConstraintGraph src){
		for(Edge e : src.edges){
			Stage a = new Stage(src.vars.get(e.s2), e.diff < 0 ? -e.diff : 0);
			Stage b = new Stage(src.vars.get(e.s1), e.diff > 0 ?  e.diff : 0);
			addConstraint(a,b);
		}
		return this;
	}
	
	public void clear(){
		for(LinkedList<Integer> l : dnNeigh){
			l.clear();
		}
		for(LinkedList<Integer> l : upNeigh){
			l.clear();
		}
		this.edges.clear();
	}
	
	public class Edge{
		public int s1,s2;
		public int diff;
		public Edge(int s1, int s2, int diff) {
			this.s1 = s1;
			this.s2 = s2;
			this.diff = diff;
		}
		
		@Override
		public boolean equals(Object obj) {
			if( !(obj instanceof Edge))
				return false;
			Edge e = (Edge) obj;
			return s1 == e.s1 && s2 == e.s2 && diff == e.diff;
		}
	}

}


